(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
 Patrice Godefroid, SAGE (systematic dynamic test generation)
 For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun T1_24515 () (_ BitVec 8))
(declare-fun T1_24391 () (_ BitVec 8))
(declare-fun T1_24387 () (_ BitVec 8))
(declare-fun T2_24305 () (_ BitVec 16))
(declare-fun T1_24296 () (_ BitVec 8))
(declare-fun T2_23904 () (_ BitVec 16))
(declare-fun T1_23895 () (_ BitVec 8))
(declare-fun T2_24389 () (_ BitVec 16))
(declare-fun T4_24297 () (_ BitVec 32))
(declare-fun T2_23853 () (_ BitVec 16))
(declare-fun T4_23845 () (_ BitVec 32))
(declare-fun T4_24292 () (_ BitVec 32))
(declare-fun T4_23840 () (_ BitVec 32))
(declare-fun T1_24389 () (_ BitVec 8))
(declare-fun T1_24390 () (_ BitVec 8))
(declare-fun T1_24305 () (_ BitVec 8))
(declare-fun T1_24306 () (_ BitVec 8))
(declare-fun T1_24297 () (_ BitVec 8))
(declare-fun T1_24298 () (_ BitVec 8))
(declare-fun T1_24299 () (_ BitVec 8))
(declare-fun T1_24300 () (_ BitVec 8))
(declare-fun T1_24292 () (_ BitVec 8))
(declare-fun T1_24293 () (_ BitVec 8))
(declare-fun T1_24294 () (_ BitVec 8))
(declare-fun T1_24295 () (_ BitVec 8))
(declare-fun T1_23904 () (_ BitVec 8))
(declare-fun T1_23905 () (_ BitVec 8))
(declare-fun T1_23853 () (_ BitVec 8))
(declare-fun T1_23854 () (_ BitVec 8))
(declare-fun T1_23845 () (_ BitVec 8))
(declare-fun T1_23846 () (_ BitVec 8))
(declare-fun T1_23847 () (_ BitVec 8))
(declare-fun T1_23848 () (_ BitVec 8))
(declare-fun T1_23840 () (_ BitVec 8))
(declare-fun T1_23841 () (_ BitVec 8))
(declare-fun T1_23842 () (_ BitVec 8))
(declare-fun T1_23843 () (_ BitVec 8))
(assert (let ((?v_12 ((_ zero_extend 24) T1_24515)) (?v_8 ((_ zero_extend 24) T1_24391)) (?v_10 ((_ zero_extend 24) T1_24387)) (?v_4 ((_ zero_extend 16) T2_24305))) (let ((?v_6 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvsub ((_ zero_extend 24) T1_23895) (_ bv8 32)) (_ bv1579205 32)) ((_ zero_extend 16) T2_23904)) (_ bv15 32)) (bvsub ((_ zero_extend 24) T1_24296) (_ bv8 32))) (_ bv2 32)) ?v_4) (_ bv7 32)) ?v_10))) (let ((?v_0 (bvsub (bvadd (bvadd ?v_6 (_ bv3 32)) ?v_8) (_ bv1579175 32)))) (let ((?v_13 (bvsub (bvadd (bvadd ?v_0 (_ bv1579176 32)) ?v_12) (_ bv1 32))) (?v_11 ((_ zero_extend 16) T2_24389)) (?v_7 (bvsub ?v_6 (_ bv1579173 32)))) (let ((?v_9 (bvsub (bvadd (bvadd ?v_7 (_ bv1579176 32)) ?v_8) (_ bv1 32))) (?v_3 ((_ zero_extend 16) T2_23853))) (let ((?v_5 (bvadd ?v_3 T4_23840)) (?v_2 (bvadd T4_23845 (_ bv1 32))) (?v_1 (bvadd T4_23845 (_ bv58690079 32)))) (and true (= T4_23840 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_23843) (_ bv8 32)) ((_ zero_extend 24) T1_23842)) (_ bv8 32)) ((_ zero_extend 24) T1_23841)) (_ bv8 32)) ((_ zero_extend 24) T1_23840))) (= T4_23845 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_23848) (_ bv8 32)) ((_ zero_extend 24) T1_23847)) (_ bv8 32)) ((_ zero_extend 24) T1_23846)) (_ bv8 32)) ((_ zero_extend 24) T1_23845))) (= T2_23853 (bvor (bvshl ((_ zero_extend 8) T1_23854) (_ bv8 16)) ((_ zero_extend 8) T1_23853))) (= T2_23904 (bvor (bvshl ((_ zero_extend 8) T1_23905) (_ bv8 16)) ((_ zero_extend 8) T1_23904))) (= T4_24292 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_24295) (_ bv8 32)) ((_ zero_extend 24) T1_24294)) (_ bv8 32)) ((_ zero_extend 24) T1_24293)) (_ bv8 32)) ((_ zero_extend 24) T1_24292))) (= T4_24297 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_24300) (_ bv8 32)) ((_ zero_extend 24) T1_24299)) (_ bv8 32)) ((_ zero_extend 24) T1_24298)) (_ bv8 32)) ((_ zero_extend 24) T1_24297))) (= T2_24305 (bvor (bvshl ((_ zero_extend 8) T1_24306) (_ bv8 16)) ((_ zero_extend 8) T1_24305))) (= T2_24389 (bvor (bvshl ((_ zero_extend 8) T1_24390) (_ bv8 16)) ((_ zero_extend 8) T1_24389))) (bvule ?v_13 (bvadd ?v_0 (_ bv1579294 32))) (not (= (bvand (bvadd ?v_3 (_ bv58690080 32)) (_ bv3 32)) (_ bv0 32))) (bvult (bvsub (_ bv112 32) ?v_2) (_ bv63 32)) (bvult (_ bv58690154 32) ?v_1) (bvult (_ bv58690090 32) ?v_1) (not (= ?v_2 (_ bv0 32))) (= T4_23840 (_ bv0 32)) (bvule ?v_3 T4_23845) (bvsle (_ bv0 32) T4_23845) (not (= ?v_5 T4_23845)) (not (= T4_23845 (_ bv0 32))) (not (= T4_23845 ?v_3)) (bvule (_ bv0 32) (bvsub ?v_4 (_ bv4 32))) (= T4_24292 ?v_5) (bvult T4_23840 T4_24292) (not (= T4_24292 T4_23840)) (= (bvadd ?v_4 T4_24292) T4_23845) (= T4_24297 T4_23845) (not (= T4_24297 (_ bv0 32))) (bvule ?v_4 (bvsub T4_23845 ?v_3)) (not (= T4_24297 ?v_4)) (bvult (bvadd ?v_7 (_ bv1579292 32)) ?v_9) (bvult (bvadd ?v_7 (_ bv1579236 32)) ?v_9) (not (= ?v_11 (_ bv0 32))) (= ?v_10 (_ bv1 32)) (= (bvadd (bvadd ?v_11 (bvsub (_ bv4294967295 32) ?v_8)) (bvsub (_ bv4294967295 32) ?v_12)) (_ bv0 32)) (bvult (bvadd ?v_0 (_ bv1579266 32)) ?v_13)))))))))
(check-sat)
(exit)
